es:ES, Q, R:(EE), A, B:Type, Ias:(AbsInterface(A) List), Ibs:(AbsInterface(B) List),
f:(E(p-first(Ias))B).
(Ia1,Ia2Ias.  Ia1  Ia2 = 0)
 (Ib1,Ib2Ibs.  Ib1  Ib2 = 0)
 (||Ias|| = ||Ibs||  )
 (i:{0..||Ias||}. Q-R-glued(es; B; f; Ias[i]; Q; Ibs[i]; R))
 (Ia1,Ia2Ias.  e, e':E. ((e  Ia1))  ((e'  Ia2))  (((Q(e,e'))) & ((Q(e',e)))))
 Q-R-glued(es; B; f; p-first(Ias); Q; p-first(Ibs); R) 

latex

Definitions

i  j < k, t  T, Y, P & Q, {i..j}, ||as||, (x,yL.  P(x;y)), P  Q, x:A. B(x), AbsInterface(A), , Top, S  T, e  X, {T}, suptype(S; T), x. t(x), P  Q, P  Q, P  Q, x,y. t(x;y), E(X), A, X  Y = 0, R1  R2, A c B, x f y, {I}, R|P, R1  R2, False, x:A. B(x), Q-R-glued(es; Ib_valtype; f; Ia; Qa; Ib; Rb), T, True, A  B, (x  l), (xL.P(x)), Dec(P), x(s), x(s1,s2), xL. P(x),

Lemmas

es-interface wf, top wf, p-first wf-interface, es-E-interface wf, length cons, select wf, es-interface-disjoint wf, le wf, length wf1, non neg length, not wf, assert wf, es-E wf, int seg wf, Q-R-glued-empty, subtype rel sum, subtype rel function, subtype rel list, es-E-interface functionality, can-apply-p-first, l exists wf, decidable assert, can-apply wf, l exists cons, es-is-interface wf, pairwise-cons, select cons tl sq, Q-R-glued-conditional, es-is-interface-p-first, es-interface-conditional-domain-iff, Q-R-glues wf, es-interface-predicate wf, rel-restriction wf, rel or wf, Q-R-glues functionality, p-first-cons, bool wf, true wf, squash wf, nat wf, select member